\documentclass{easychair}

\usepackage{hyperref}

\title{The OpenSMT Solver in SMT-COMP 2019}
\author{
Martin Blicha \and 
Antti E. J. Hyv{\"a}rinen \and
Matteo Marescotti \and
Natasha Sharygina \\
}
\institute{Universit{\`a} della Svizzera italiana (USI), Lugano,
Switzerland}
\date{}
\titlerunning{The OpenSMT Solver in SMT-COMP 2019}
\authorrunning{M. Blicha, A. E. J. Hyv{\"a}rinen, M. Marescotti, and N.
Sharygina}
\begin{document}
\maketitle

\section{Overview}

OpenSMT~\cite{HyvarinenMAS16} is a T-DPLL based SMT
solver~\cite{NieuwenhuisOT:JACM06} that has been developed at USI,
Switzerland, since 2008.  The solver is written in {\tt C++} and
currently supports the quantifier-free logics of equality with
uninterpreted functions (QF\_UF), and linear real arithmetic (QF\_LRA).
The solver has a rudimentary support for quantifier-free linear integer
arithmetic (QF\_LIA) based on branch-and-bound, and supports some
aspects of bit-vector logic (QF\_BV).

In comparison to 2018, the 2019 competition entry features a wide range
of performance improvements in simplification, the Simplex
algorithm~\cite{DutertreM:CAV06}, and the Egraph
algorithm~\cite{DetlefsNS:JAC05}, several bug fixes related to solver
soundness, and improved support for the logics.  In the process, the
solver high-level architecture improved and low-level code cleaning
resulted in fewer compiler warnings.

The solver development process is better defined in comparison to the
previous state.  The main public repository
 is now
hosted in GitHub, where the commit process is integrated with Travis CI
to ensure the passing of regression tests and different compilation.
Commits are integrated to the master branch through pull requests once
they pass a human review and the Travis CI configuration.

OpenSMT features not exercised in the competition include support for a
wide range of interpolation algorithms for propositional
logic~\cite{AltFHS:VSTTE2015}, linear real
arithmetic~\cite{BlichaHKS19}, and uninterpreted
functions~\cite{AltHAS:FMCAD17}; an experimental look\-ahead-based
search algorithm~\cite{HyvarinenMSCS18} as an alternative to the more
standard CDCL algorithm; and features that support search-space
partitioning in particular designed for parallel
solving~\cite{HyvarinenMS:SAT15}.

\section{External Code and Contributors}

The SAT solver driving OpenSMT is based on the MiniSAT
solver~\cite{EenS:SAT03}, and the rational number implementation is
inspired by a library written by David Monniaux.  Several people have
directly contributed to the OpenSMT code.  In alphabetical order, the
major contributors are
%
Leonardo Alt (Ethereum Foundation),
Sepideh Asadi (USI),
Martin Blicha (USI, Charles University),
Roberto Bruttomesso (Cybersecurity / Nozomi Networks),
Antti E. J. Hyv{\"a}rinen (USI),
Matteo Marescotti (USI),
Edgar Pek (University of Illinois, Urbana-Champaign),
Simone Fulvio Rollini (United Technologies Research Center),
Parvin Sadigova (King's College London), and
Aliaksei Tsitovich (Sonova).
%
The solver is being developed in Natasha Sharygina's software
verification group at USI.

\section{Utilization}

OpenSMT is used in a range of projects as a back-end solver.  Recent
examples include its use as an interpolation engine of the Sally model
checker~\cite{JovanovicD:FMCAD16} which won the transition systems
category in the constrained Horn clause competition 2019.  OpenSMT also
forms the basis of our own model checkers such as
HiFrog~\cite{AltACMFHS17}.  OpenSMT is compatible with the SMTS
parallelization framework~\cite{MarescottiHS18}.

\section{Availability}
The source code repository and more information on the solver is
available at

\begin{itemize}
    \item \url{https://github.com/usi-verification-and-security/opensmt}
        and
    \item \url{http://verify.inf.usi.ch/opensmt}
\end{itemize}

\iffalse
in chronological order, work on interpolation 
algorithms~\cite{BlichaHKS19,AltHAS17,JancikAFHKS16,AsadiBFHESC18}
and parallel SMT 
solving~\cite{HyvarinenMSCS18,MarescottiHS18,HyvarinenMS:SAT15}.
OpenSMT2 is
used as the back-end in model-checking tools
HiFrog~\cite{AltACMFHS17},
eVolCheck~\cite{FSS_TACAS13}, 
FunFrog~\cite{SFS_ATVA12}, and
PeRIPLO~\cite{RolliniAFHS:LPAR2013,AltFHS:VSTTE2015}.
OpenSMT2 is a supported engine in the parallel 
solving framework SMTS~\cite{MarescottiHS16}.

\section{Acknowledgements}
We thank everyone who helped
developing OpenSMT2. In particular,
Leonardo Alt,
Sepideh Asadi,
Martin Blicha,
Roberto Bruttomesso,
Antti E. J. Hyv{\"a}rinen,
Matteo Marescotti,
Edgar Pek,
Simone Fulvio Rollini, 
Parvin Sadigova,
Natasha Sharygina,
Aliaksei Tsitovich.
\fi

\bibliography{abstract}
\bibliographystyle{plain}

\end{document}
